l:IdLnk, dt:fpf(Id; tg.Type), tg:Id, T:Type.
sqequal(fpf-cap(lnk-decl(l; dt); Kind-deq; rcv(l,tg); T); fpf-cap(dt; id-deq; tg; T)) 

latex

Definitions	x:A. B(x), t  T, x. t(x), fpf-cap(f; eq; x; z), if b then t else f fi , P  Q, tt, ff, prop{i:l}, rcv(l,tg), lnk-decl(l; dt), fpf-ap(f; eq; x), t.2, outl(x), fpf-dom(eq; x; f), t.1, guard(T), sq_type(T), x:A. B(x), P  Q, x(s), , Unit, P  Q, A, False, fpf(A; a.B(a)), P  Q,
Lemmas	Id wf, fpf wf, IdLnk wf, fpf-dom wf, Knd wf, Kind-deq wf, lnk-decl wf, fpf-trivial-subtype-top, top wf, rcv wf, bool wf, eqtt to assert, id-deq wf, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, assert-deq-member, map wf, member map, rcv one one, Id sq, l member wf